Nuprl Lemma : length_zip
4,23
postcript
pdf
T1
,
T2
:Type,
as
:
T1
List,
bs
:
T2
List. ||
as
|| = ||
bs
||
||zip(
as
;
bs
)|| = ||
as
||
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
Prop
,
P
Q
,
{
T
}
Lemmas
length
wf1
origin
T1, T2:Type, as:T1 List, bs:T2 List. ||as|| = ||bs|| 
||zip(as;bs)|| = ||as|| T1, T2:Type, as:T1 List, bs:T2 List. ||as|| = ||bs|| ||zip(as;bs)|| = ||as|| Tx:A. B(x) Q